1  /-
  2  Copyright (c) 2018 Chris Hughes. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Chris Hughes
  5  -/
  6  import group_theory.group_action group_theory.quotient_group
src         └───────────────────────┘ └─────────────────────────┘
  7  import group_theory.order_of_element data.zmod.basic
src         └───────────────────────────┘ └─────────────┘
  8  
  9  open equiv fintype finset mul_action function
 10  open equiv.perm is_subgroup list quotient_group
 11  universes u v w
 12  variables {G : Type u} {α : Type v} {β : Type w} [group G]
id                                                   └───┘
src                                                    └───┘
typ                                                  └───┘
 13  
 14  local attribute [instance, priority 10] subtype.fintype set_fintype classical.prop_decidable
id                                           └─────────────┘ └─────────┘ └──────────────────────┘
src                                          └─────────────┘ └─────────┘ └──────────────────────┘
typ                                          └─────────────┘ └─────────┘ └──────────────────────┘
 15  
 16  namespace mul_action
 17  variables [mul_action G α]
id              └────────┘
src             └────────┘
typ             └────────┘
doc             └────────┘
 18  
 19  lemma mem_fixed_points_iff_card_orbit_eq_one {a : α}
id                                                     
typ                                                    
 20    [fintype (orbit G a)] : a ∈ fixed_points G α ↔ card (orbit G a) = 1 :=
id      └─────┘  └───┘         └──────────┘    └──┘  └───┘    
src     └─────┘  └───┘            └──────────┘      └──┘  └───┘      
typ     └─────┘  └───┘         └──────────┘    └──┘  └───┘    
doc     └─────┘                                       └──┘
 21  begin
st   └─────
 22    rw [fintype.card_eq_one_iff, mem_fixed_points],
id         └─────────────────────┘  └──────────────┘
src    └──┘└─────────────────────┘└┘└──────────────┘
typ    └──┘└─────────────────────┘└┘└──────────────┘
doc    └──┘                       └┘                
txt    └──┘                       └┘                
par    └──┘                       └┘                
pid      └┘                       └┘                
st   ────────────────────────────┘└────────────────┘└──
 23    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
 24    { exact λ h, ⟨⟨a, mem_orbit_self _⟩, λ ⟨b, ⟨x, hx⟩⟩, subtype.eq $ by simp [h x, hx.symm]⟩ },
id                      └────────────┘                     └────────┘             
src      └────┘ └──┘   └┘└────────────┘└───┘ └┘ └┘  └┘  └──┘└────────┘   └────┘  └┘       └┘
typ      └────┘ └──┘  └┘└────────────┘└───┘ └┘ └┘  └┘  └──┘└────────┘   └────┘└┘└─────┘└┘
doc      └────┘ └──┘   └┘              └───┘ └┘ └┘  └┘  └──┘             └────┘  └┘       └┘
txt      └────┘ └──┘   └┘              └───┘ └┘ └┘  └┘  └──┘             └────┘  └┘       └┘
par      └────┘ └──┘   └┘              └───┘ └┘ └┘  └┘  └──┘             └────┘  └┘       └┘
pid            └──┘   └┘              └───┘ └┘ └┘  └┘  └──┘             └─────┘  └┘       └┘
st   ───┘└────────────────────────────────────────────────────────────────┘└──────────────────┘└┘└┘
 25    { assume h x,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid      └────────┘
st   ─────────────┘└─
 26      rcases h with ⟨⟨z, hz⟩, hz₁⟩,
id              
src      └─────┘ └──────────────────┘
typ      └─────┘└──────────────────┘
doc      └─────┘ └──────────────────┘
txt      └─────┘ └──────────────────┘
par      └─────┘ └──────────────────┘
pid             └──────────────────┘
st   ───────────────────────────────┘└─
 27      exact calc x • a = z : subtype.mk.inj (hz₁ ⟨x • a, mem_orbit _ _⟩)
id                                                       └───────┘
src      └────┘        └─┘                      └┘└───────┘└──────
typ      └────┘       └─┘                     └┘└───────┘└──────
doc      └────┘         └─┘                      └┘         └──────
txt      └────┘         └─┘                      └┘         └──────
par      └────┘         └─┘                      └┘         └──────
pid                    └─┘                      └┘         └──────
st   ───────────────────────────────────────────────────────────────────────
 28        ... = a : (subtype.mk.inj (hz₁ ⟨a, mem_orbit_self _⟩)).symm }
id                    └────────────┘  └─┘    └────────────┘
src  ─────────┘  └─┘ └────────────┘      └┘└────────────┘└─────────┘
typ  ─────────┘  └─┘ └────────────┘ └─┘ └┘└────────────┘└─────────┘
doc  ─────────┘  └─┘                     └┘              └─────────┘
txt  ─────────┘  └─┘                     └┘              └─────────┘
par  ─────────┘  └─┘                     └┘              └─────────┘
pid  ─────────┘  └─┘                     └┘              └───────┘└┘
st   ─────────────────────────────────────────────────────────────────┘└─
 29  end
st   ──┘
 30  
 31  lemma card_modeq_card_fixed_points [fintype α] [fintype G] [fintype (fixed_points G α)]
id                                       └─────┘    └─────┘    └─────┘  └──────────┘  
src                                      └─────┘     └─────┘     └─────┘  └──────────┘
typ                                      └─────┘    └─────┘    └─────┘  └──────────┘  
doc                                      └─────┘     └─────┘     └─────┘
 32    {p n : ℕ} (hp : nat.prime p) (h : card G = p ^ n) : card α ≡ card (fixed_points G α) [MOD p] :=
id                    └───────┘        └──┘         └──┘   └──┘  └──────────┘    └──┘ 
src                   └───────┘         └──┘            └──┘    └──┘  └──────────┘      └──┘  
typ                   └───────┘        └──┘         └──┘   └──┘  └──────────┘    └──┘ 
doc                    └───────┘         └──┘              └──┘    └──┘                    └──┘  
 33  calc card α = card (Σ y : quotient (orbit_rel G α), {x // quotient.mk' x = y}) :
id        └──┘    └──┘       └──────┘  └───────┘        └──────────┘   
src       └──┘     └──┘       └──────┘  └───────┘           └──────────┘   
typ       └──┘    └──┘       └──────┘  └───────┘        └──────────┘   
doc       └──┘     └──┘
 34    card_congr (sigma_preimage_equiv (@quotient.mk' _ (orbit_rel G α))).symm
id     └────────┘  └──────────────────┘   └──────────┘    └───────┘     └──┘
src    └────────┘  └──────────────────┘   └──────────┘    └───────┘       └──┘
typ    └────────┘  └──────────────────┘   └──────────┘    └───────┘     └──┘
 35  ... = univ.sum (λ a : quotient (orbit_rel G α), card {x // quotient.mk' x = a}) : card_sigma _
id         └──┘└──┘        └──────┘  └───────┘     └──┘     └──────────┘        └────────┘
src        └──┘└──┘        └──────┘  └───────┘       └──┘      └──────────┘          └────────┘
typ        └──┘└──┘        └──────┘  └───────┘     └──┘     └──────────┘        └────────┘
doc        └──┘                                      └──┘
 36  ... ≡ (@univ (fixed_points G α) _).sum (λ _, 1) [MOD p] :
id           └──┘  └──────────┘      └─┘     
src          └──┘  └──────────┘        └─┘
typ          └──┘  └──────────┘      └─┘     
doc          └──┘
 37  begin
st   └─────
 38    rw [← zmodp.eq_iff_modeq_nat hp, sum_nat_cast, sum_nat_cast],
id           └────────────────────┘ └┘  └──────────┘  └──────────┘
src    └────┘└────────────────────┘  └┘└──────────┘└┘└──────────┘
typ    └────┘└────────────────────┘└┘└┘└──────────┘└┘└──────────┘
doc    └────┘                        └┘            └┘            
txt    └────┘                        └┘            └┘            
par    └────┘                        └┘            └┘            
pid      └──┘                        └┘            └┘            
st   ────────────────────────────────┘└────────────┘└────────────┘└──
 39    refine eq.symm (sum_bij_ne_zero (λ a _ _, quotient.mk' a.1)
id            └─────┘  └─────────────┘           └──────────┘
src    └─────┘└─────┘ └─────────────┘  └──────┘└──────────┘ └───
typ    └─────┘└─────┘ └─────────────┘  └──────┘└──────────┘ └───
doc    └─────┘                         └──────┘             └───
txt    └─────┘                         └──────┘             └───
par    └─────┘                         └──────┘             └───
pid                                   └──────┘             └───
st   ──────────────────────────────────────────────────────────────
 40      (λ _ _ _, mem_univ _)
id                 └──────┘
src  ───┘  └──────┘└──────┘└───
typ  ───┘  └──────┘└──────┘└───
doc  ───┘  └──────┘        └───
txt  ───┘  └──────┘        └───
par  ───┘  └──────┘        └───
pid  ───┘  └──────┘        └───
st   ──────────────────────────
 41      (λ a₁ a₂ _ _ _ _ h,
src  ───┘  └─────────────────
typ  ───┘  └─────────────────
doc  ───┘  └─────────────────
txt  ───┘  └─────────────────
par  ───┘  └─────────────────
pid  ───┘  └─────────────────
st   ────────────────────────
 42        subtype.eq ((mem_fixed_points' α).1 a₂.2 a₁.1 (quotient.exact' h)))
id         └────────┘   └───────────────┘                └─────────────┘
src  ─────┘└────────┘  └───────────────┘ └──┘  └─┘  └─┘ └─────────────┘ └───
typ  ─────┘└────────┘  └───────────────┘└──┘  └─┘  └─┘ └─────────────┘ └───
doc  ─────┘                              └──┘  └─┘  └─┘                 └───
txt  ─────┘                              └──┘  └─┘  └─┘                 └───
par  ─────┘                              └──┘  └─┘  └─┘                 └───
pid  ─────┘                              └──┘  └─┘  └─┘                 └───
st   ──────────────────────────────────────────────────────────────────────────
 43        (λ b, _)
src  ─────┘  └──────
typ  ─────┘  └──────
doc  ─────┘  └──────
txt  ─────┘  └──────
par  ─────┘  └──────
pid  ─────┘  └──────
st   ───────────────
 44        (λ a ha _, by rw [← mem_fixed_points_iff_card_orbit_eq_one.1 a.2];
id                             └────────────────────────────────────┘   
src  ─────┘  └───────┘  └────┘└────────────────────────────────────┘└─┘ └─┘└─
typ  ─────┘  └───────┘  └────┘└────────────────────────────────────┘└─┘└─┘└─
doc  ─────┘  └───────┘  └────┘                                      └─┘ └─┘└─
txt  ─────┘  └───────┘  └────┘                                      └─┘ └─┘└─
par  ─────┘  └───────┘  └────┘                                      └─┘ └─┘└─
pid  ─────┘  └───────┘  └─────┘                                      └─┘ └────
st   ──────────────────┘└───────────────────────────────────────────────┘└─┘└─
 45          simp only [quotient.eq']; congr)),
id                      └──────────┘
src  ───────┘└─────────┘└──────────┘└┘└───┘└┘
typ  ───────┘└─────────┘└──────────┘└┘└───┘└┘
doc  ───────┘└─────────┘            └┘     └┘
txt  ───────┘└─────────┘            └┘└───┘└┘
par  ───────┘└─────────┘            └┘└───┘└┘
pid  ──────────────────┘            └────────┘
st   ──────────────────────────────────────┘└┘└─
 46    { refine quotient.induction_on' b (λ b _ hb, _),
id              └────────────────────┘ 
src      └─────┘└────────────────────┘   └─────────┘
typ      └─────┘└────────────────────┘  └─────────┘
doc      └─────┘                         └─────────┘
txt      └─────┘                         └─────────┘
par      └─────┘                         └─────────┘
pid                                     └─────────┘
st   ────────────────────────────────────────────────┘└─
 47      have : card (orbit G b) ∣ p ^ n,
id              └──┘  └───┘       
src      └─────┘└──┘ └───┘  └┘ 
typ      └─────┘└──┘ └───┘└┘
doc      └─────┘└──┘        └┘   
txt      └─────┘            └┘   
par      └─────┘            └┘   
pid      └───┘└┘            └┘   
st   ──────────────────────────────────┘└─
 48      { rw [← h, fintype.card_congr (orbit_equiv_quotient_stabilizer G b)];
id                 └────────────────┘  └─────────────────────────────┘  
src        └────┘ └┘└────────────────┘ └─────────────────────────────┘  └┘
typ        └────┘└┘└────────────────┘ └─────────────────────────────┘└┘
doc        └────┘ └┘                                                    └┘
txt        └────┘ └┘                                                    └┘
par        └────┘ └┘                                                    └┘
pid          └──┘ └┘                                                    └┘
st   ─────┘└─────┘└────────────────────────────────────────────────────────┘└─
 49        exact card_quotient_dvd_card _ },
id               └────────────────────┘
src        └────┘└────────────────────┘└─┘
typ        └────┘└────────────────────┘└─┘
doc        └────┘                      └─┘
txt        └────┘                      └─┘
par        └────┘                      └─┘
pid                                   └┘
st   ────────────────────────────────────┘└┘
 50      rcases (nat.dvd_prime_pow hp).1 this with ⟨k, _, hk⟩,
id               └───────────────┘ └┘    └──┘
src      └─────┘ └───────────────┘  └──┘    └──────────────┘
typ      └─────┘ └───────────────┘└┘└──┘└──┘└──────────────┘
doc      └─────┘                    └──┘    └──────────────┘
txt      └─────┘                    └──┘    └──────────────┘
par      └─────┘                    └──┘    └──────────────┘
pid                                └──┘    └──────────────┘
st   ───────────────────────────────────────────────────────┘└─
 51      have hb' :¬ p ^ 1 ∣ p ^ k,
id                              
src      └────────┘   └─┘   
typ      └────────┘   └─┘  
doc      └────────┘   └─┘   
txt      └────────┘   └─┘   
par      └────────┘   └─┘   
pid      └──────┘└┘   └─┘   
st   ────────────────────────────┘└─
 52      { rw [nat.pow_one, ← hk, ← nat.modeq.modeq_zero_iff, ← zmodp.eq_iff_modeq_nat hp,
id             └─────────┘    └┘    └──────────────────────┘    └────────────────────┘ └┘
src        └──┘└─────────┘└──┘  └──┘└──────────────────────┘└──┘└────────────────────┘  └─
typ        └──┘└─────────┘└──┘└┘└──┘└──────────────────────┘└──┘└────────────────────┘└┘└─
doc        └──┘           └──┘  └──┘                        └──┘                        └─
txt        └──┘           └──┘  └──┘                        └──┘                        └─
par        └──┘           └──┘  └──┘                        └──┘                        └─
pid          └┘           └──┘  └──┘                        └──┘                        └─
st   ─────┘└─────────────┘└────┘└──────────────────────────┘└───────────────────────────┘└─
 53          nat.cast_zero, ← ne.def],
id           └───────────┘    └────┘
src  ───────┘└───────────┘└──┘└────┘
typ  ───────┘└───────────┘└──┘└────┘
doc  ───────┘             └──┘      
txt  ───────┘             └──┘      
par  ───────┘             └──┘      
pid  ───────┘             └──┘      
st   ────────────────────┘└────────┘└──
 54        exact eq.mpr (by simp only [quotient.eq']; congr) hb },
id               └────┘                └──────────┘          └┘
src        └────┘└────┘   └─────────┘└──────────┘└┘└───┘└┘  
typ        └────┘└────┘   └─────────┘└──────────┘└┘└───┘└┘└┘
doc        └────┘         └─────────┘            └┘     └┘  
txt        └────┘         └─────────┘            └┘└───┘└┘  
par        └────┘         └─────────┘            └┘└───┘└┘  
pid                      └──────────┘            └────────┘  
st   ─────────────────────┘└──────────────────────────────┘└───┘└┘
 55      have : k = 0 := nat.le_zero_iff.1 (nat.le_of_lt_succ (lt_of_not_ge (mt (nat.pow_dvd_pow p) hb'))),
id                     └─────────────┘    └───────────────┘  └──────────┘  └┘  └─────────────┘   └─┘
src      └─────┘ └────┘└─────────────┘└─┘ └───────────────┘ └──────────┘ └┘ └─────────────┘ └┘   └─┘
typ      └─────┘└────┘└─────────────┘└─┘ └───────────────┘ └──────────┘ └┘ └─────────────┘└┘└─┘└─┘
doc      └─────┘  └────┘               └─┘                                                   └┘   └─┘
txt      └─────┘  └────┘               └─┘                                                   └┘   └─┘
par      └─────┘  └────┘               └─┘                                                   └┘   └─┘
pid      └───┘└┘  └───┘               └─┘                                                   └┘   └─┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
 56      refine ⟨⟨b, mem_fixed_points_iff_card_orbit_eq_one.2 $ by rw [hk, this, nat.pow_zero]⟩, mem_univ _,
id                  └────────────────────────────────────┘            └┘  └──┘  └──────────┘    └──────┘
src      └─────┘   └┘└────────────────────────────────────┘└─┘   └──┘  └┘    └┘└──────────┘└─┘└──────┘└───
typ      └─────┘  └┘└────────────────────────────────────┘└─┘   └──┘└┘└┘└──┘└┘└──────────┘└─┘└──────┘└───
doc      └─────┘   └┘                                      └─┘   └──┘  └┘    └┘            └─┘        └───
txt      └─────┘   └┘                                      └─┘   └──┘  └┘    └┘            └─┘        └───
par      └─────┘   └┘                                      └─┘   └──┘  └┘    └┘            └─┘        └───
pid               └┘                                      └─┘   └───┘  └┘    └┘            └──┘        └───
st   ────────────────────────────────────────────────────────────┘└─────┘└────┘└────────────┘└──────────────
 57        by simp [zero_ne_one], rfl⟩ }
id                  └─────────┘   └─┘
src  ─────┘  └────┘└─────────┘└┘└─┘└┘
typ  ─────┘  └────┘└─────────┘└┘└─┘└┘
doc  ─────┘  └────┘           └┘   └┘
txt  ─────┘  └────┘           └┘   └┘
par  ─────┘  └────┘           └┘   └┘
pid  ─────┘  └─────┘           └─┘   
st   ───────┘└─────────────────┘└─────┘└─
 58  end
st   ──┘
 59  ... = _ : by simp; refl
src               └──┘  └────
typ               └──┘  └────
doc               └──┘  └────
txt               └──┘  └────
par               └──┘  └────
pid                         
st               └───────────
 60  
src  
typ  
doc  
txt  
par  
pid  
st   
 61  end mul_action
 62  
 63  lemma quotient_group.card_preimage_mk [fintype G] (s : set G) [is_subgroup s]
id                                          └─────┘        └─┘    └─────────┘ 
src                                         └─────┘         └─┘     └─────────┘
typ                                         └─────┘        └─┘    └─────────┘ 
doc                                         └─────┘                 └─────────┘
 64    (t : set (quotient s)) : fintype.card (quotient_group.mk ⁻¹' t) =
id          └─┘  └──────┘      └──────────┘  └───────────────┘ └─┘   
src         └─┘  └──────┘       └──────────┘  └───────────────┘ └─┘    
typ         └─┘  └──────┘      └──────────┘  └───────────────┘ └─┘   
doc              └──────┘       └──────────┘                    └─┘
 65    fintype.card s * fintype.card t :=
id     └──────────┘   └──────────┘ 
src    └──────────┘    └──────────┘
typ    └──────────┘   └──────────┘ 
doc    └──────────┘     └──────────┘
 66  by rw [← fintype.card_prod, fintype.card_congr
id            └───────────────┘  └────────────────┘
src     └────┘└───────────────┘└┘└────────────────┘
typ     └────┘└───────────────┘└┘└────────────────┘
doc     └────┘                 └┘                  
txt     └────┘                 └┘                  
par     └────┘                 └┘                  
pid       └──┘                 └┘                  
st     └──────────────────────┘└────────────────────
 67    (preimage_mk_equiv_subgroup_times_set _ _)]
id      └──────────────────────────────────┘
src  ─┘ └──────────────────────────────────┘└──────
typ  ─┘ └──────────────────────────────────┘└──────
doc  ─┘                                     └──────
txt  ─┘                                     └──────
par  ─┘                                     └──────
pid  ─┘                                     └────┘
st   ───────────────────────────────────────────┘
 68  
src  
typ  
doc  
txt  
par  
pid  
st   
 69  namespace sylow
 70  
 71  def mk_vector_prod_eq_one (n : ℕ) (v : vector G n) : vector G (n+1) :=
id                                         └────┘      └────┘   
src                                        └────┘        └────┘     
typ                                        └────┘      └────┘   
 72  v.to_list.prod⁻¹ :: v
id   └──────┘└───┘└┘ └┘ 
src   └──────┘└───┘└┘ └┘
typ  └──────┘└───┘└┘ └┘ 
doc           └───┘
 73  
 74  lemma mk_vector_prod_eq_one_inj (n : ℕ) : injective (@mk_vector_prod_eq_one G _ n) :=
id                                            └───────┘   └───────────────────┘    
src                                           └───────┘   └───────────────────┘
typ                                           └───────┘   └───────────────────┘    
 75  λ ⟨v, _⟩ ⟨w, _⟩ h, subtype.eq (show v = w, by injection h with h; injection h)
id                 └────────┘                                             
src                     └────────┘                └────────┘ └─────┘  └────────┘
typ                └────────┘                └────────┘└─────┘  └────────┘
doc                                                └────────┘ └─────┘  └────────┘
txt                                                └────────┘ └─────┘  └────────┘
par                                                └────────┘ └─────┘  └────────┘
pid                                                          └─────┘           
st                                                └──────────────────────────────┘
 76  
 77  def vectors_prod_eq_one (G : Type*) [group G] (n : ℕ) : set (vector G n) :=
id                                        └───┘            └─┘  └────┘  
src                                       └───┘             └─┘  └────┘
typ                                       └───┘            └─┘  └────┘  
 78  {v | v.to_list.prod = 1}
id      └──────┘└───┘ 
src       └──────┘└───┘ 
typ     └──────┘└───┘ 
doc                └───┘
 79  
 80  lemma mem_vectors_prod_eq_one {n : ℕ} (v : vector G n) :
id                                             └────┘  
src                                            └────┘
typ                                            └────┘  
 81    v ∈ vectors_prod_eq_one G n ↔ v.to_list.prod = 1 := iff.rfl
id       └─────────────────┘    └──────┘└───┘       └─────┘
src       └─────────────────┘       └──────┘└───┘       └─────┘
typ      └─────────────────┘    └──────┘└───┘       └─────┘
doc                                           └───┘
 82  
 83  lemma mem_vectors_prod_eq_one_iff {n : ℕ} (v : vector G (n + 1)) :
id                                                 └────┘    
src                                                └────┘      
typ                                                └────┘    
 84    v ∈ vectors_prod_eq_one G (n + 1) ↔ v ∈ set.range (@mk_vector_prod_eq_one G _ n) :=
id       └─────────────────┘           └───────┘   └───────────────────┘    
src       └─────────────────┘              └───────┘   └───────────────────┘
typ      └─────────────────┘           └───────┘   └───────────────────┘    
doc                                            └───────┘
 85  ⟨λ (h : v.to_list.prod = 1), ⟨v.tail,
id           └──────┘└───┘       └───┘
src           └──────┘└───┘        └───┘
typ          └──────┘└───┘       └───┘
doc                   └───┘
 86    begin
st     └─────
 87      unfold mk_vector_prod_eq_one,
src      └──────────────────────────┘
typ      └──────────────────────────┘
doc      └──────────────────────────┘
txt      └──────────────────────────┘
par      └──────────────────────────┘
pid            └────────────────────┘
st   ───────────────────────────────┘└─
 88      conv {to_rhs, rw ← vector.cons_head_tail v},
id                          └───────────────────┘ 
src      └────┘└────┘└┘└───┘└───────────────────┘ 
typ      └────┘└────┘└┘└───┘└───────────────────┘
txt      └────┘└────┘└┘└───┘                      
par      └────┘└────┘└┘└───┘                      
pid          └────────────┘                      
st   ─────────┘└────┘└────────────────────────────┘└┘
 89      suffices : (v.tail.to_list.prod)⁻¹ = v.head,
id                   └─────────────────┘ └┘  └────┘
src      └─────────┘ └─────────────────┘└┘└────┘
typ      └─────────┘ └─────────────────┘└┘└────┘
doc      └─────────┘ └─────────────────┘   
txt      └─────────┘                       
par      └─────────┘                       
pid      └───────┘└┘                       
st   ──────────────────────────────────────────────┘└─
 90      { rw this },
id            └──┘
src        └─┘    
typ        └─┘└──┘
doc        └─┘    
txt        └─┘    
par        └─┘    
pid              
st   ─────┘└──────┘└┘
 91      rw [← mul_right_inj v.tail.to_list.prod, inv_mul_self, ← list.prod_cons,
id             └───────────┘ └─────────────────┘  └──────────┘    └────────────┘
src      └────┘└───────────┘└─────────────────┘└┘└──────────┘└──┘└────────────┘└─
typ      └────┘└───────────┘└─────────────────┘└┘└──────────┘└──┘└────────────┘└─
doc      └────┘             └─────────────────┘└┘            └──┘              └─
txt      └────┘                                └┘            └──┘              └─
par      └────┘                                └┘            └──┘              └─
pid        └──┘                                └┘            └──┘              └─
st   ──────────────────────────────────────────┘└────────────┘└────────────────┘└─
 92        ← vector.to_list_cons, vector.cons_head_tail, h]
id           └─────────────────┘  └───────────────────┘  
src  ───────┘└─────────────────┘└┘└───────────────────┘└┘ └─
typ  ───────┘└─────────────────┘└┘└───────────────────┘└┘└─
doc  ───────┘                   └┘                     └┘ └─
txt  ───────┘                   └┘                     └┘ └─
par  ───────┘                   └┘                     └┘ └─
pid  ───────┘                   └┘                     └┘ 
st   ──────────────────────────┘└─────────────────────┘└─┘
 93    end⟩,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
 94    λ ⟨w, hw⟩, by rw [mem_vectors_prod_eq_one, ← hw, mk_vector_prod_eq_one,
id                      └─────────────────────┘    └┘  └───────────────────┘
src                  └──┘└─────────────────────┘└──┘  └┘└───────────────────┘└─
typ                 └──┘└─────────────────────┘└──┘└┘└┘└───────────────────┘└─
doc                  └──┘                       └──┘  └┘                     └─
txt                  └──┘                       └──┘  └┘                     └─
par                  └──┘                       └──┘  └┘                     └─
pid                    └┘                       └──┘  └┘                     └─
st                  └──────────────────────────┘└────┘└─────────────────────┘└─
 95      vector.to_list_cons, list.prod_cons, inv_mul_self]⟩
id       └─────────────────┘  └────────────┘  └──────────┘
src  ───┘└─────────────────┘└┘└────────────┘└┘└──────────┘
typ  ───┘└─────────────────┘└┘└────────────┘└┘└──────────┘
doc  ───┘                   └┘              └┘            
txt  ───┘                   └┘              └┘            
par  ───┘                   └┘              └┘            
pid  ───┘                   └┘              └┘            
st   ──────────────────────┘└──────────────┘└────────────┘
 96  
 97  def rotate_vectors_prod_eq_one (G : Type*) [group G] (n : ℕ+) (m : multiplicative (zmod n))
id                                               └───┘        └┘       └────────────┘  └──┘ 
src                                              └───┘         └┘       └────────────┘  └──┘
typ                                              └───┘        └┘       └────────────┘  └──┘ 
doc                                                            └┘
 98    (v : vectors_prod_eq_one G n) : vectors_prod_eq_one G n :=
id          └─────────────────┘      └─────────────────┘  
src         └─────────────────┘        └─────────────────┘
typ         └─────────────────┘      └─────────────────┘  
 99  ⟨⟨v.1.to_list.rotate m.1, by simp⟩, prod_rotate_eq_one_of_prod_eq_one v.2 _⟩
id      └─────┘ └────┘               └───────────────────────────────┘ 
src      └─────┘ └────┘         └──┘   └───────────────────────────────┘  
typ     └─────┘ └────┘        └──┘   └───────────────────────────────┘ 
doc               └────┘          └──┘
txt                               └──┘
par                               └──┘
st                               └───┘
100  
101  instance rotate_vectors_prod_eq_one.mul_action (n : ℕ+) :
id                                                       └┘
src                                                      └┘
typ                                                      └┘
doc                                                      └┘
102    mul_action (multiplicative (zmod n)) (vectors_prod_eq_one G n) :=
id     └────────┘  └────────────┘  └──┘     └─────────────────┘  
src    └────────┘  └────────────┘  └──┘      └─────────────────┘
typ    └────────┘  └────────────┘  └──┘     └─────────────────┘  
doc    └────────┘
103  { smul := (rotate_vectors_prod_eq_one G n),
id              └────────────────────────┘  
src             └────────────────────────┘
typ             └────────────────────────┘  
104    one_smul := λ v, subtype.eq $ vector.eq _ _ $ rotate_zero v.1.to_list,
id                     └────────┘   └───────┘       └─────────┘  └─────┘
src                     └────────┘   └───────┘       └─────────┘   └─────┘
typ                    └────────┘   └───────┘       └─────────┘  └─────┘
105    mul_smul := λ a b ⟨⟨v, hv₁⟩, hv₂⟩, subtype.eq $ vector.eq _ _ $
id                                    └────────┘   └───────┘
src                                       └────────┘   └───────┘
typ                                   └────────┘   └───────┘
106      show v.rotate ((a + b : zmod n).val) = list.rotate (list.rotate v (b.val)) (a.val),
id             └─────┘        └──┘  └─┘    └─────────┘  └─────────┘    └──┘    └──┘
src            └─────┘          └──┘   └─┘    └─────────┘  └─────────┘     └──┘     └──┘
typ            └─────┘        └──┘  └─┘    └─────────┘  └─────────┘    └──┘    └──┘
doc            └─────┘                          └─────────┘  └─────────┘
107      by rw [zmod.add_val, rotate_rotate, ← rotate_mod _ (b.1 + a.1), add_comm, hv₁] }
id              └──────────┘  └───────────┘    └────────┘             └──────┘  └─┘
src         └──┘└──────────┘└┘└───────────┘└──┘└────────┘└─┘  └─┘ └───┘└──────┘└┘   └┘
typ         └──┘└──────────┘└┘└───────────┘└──┘└────────┘└─┘ └─┘└───┘└──────┘└┘└─┘└┘
doc         └──┘            └┘             └──┘          └─┘  └─┘  └───┘        └┘   └┘
txt         └──┘            └┘             └──┘          └─┘  └─┘  └───┘        └┘   └┘
par         └──┘            └┘             └──┘          └─┘  └─┘  └───┘        └┘   └┘
pid           └┘            └┘             └──┘          └─┘  └─┘  └───┘        └┘   
st         └───────────────┘└─────────────┘└──────────────────────────┘└────────┘└───┘
108  
109  lemma one_mem_vectors_prod_eq_one (n : ℕ) : vector.repeat (1 : G) n ∈ vectors_prod_eq_one G n :=
id                                              └───────────┘          └─────────────────┘  
src                                             └───────────┘            └─────────────────┘
typ                                             └───────────┘          └─────────────────┘  
110  by simp [vector.repeat, vectors_prod_eq_one]
id            └───────────┘  └─────────────────┘
src     └────┘└───────────┘└┘└─────────────────┘└─
typ     └────┘└───────────┘└┘└─────────────────┘└─
doc     └────┘             └┘                   └─
txt     └────┘             └┘                   └─
par     └────┘             └┘                   └─
pid                      └┘                   
st     └──────────────────────────────────────────
111  
src  
typ  
doc  
txt  
par  
pid  
st   
112  lemma one_mem_fixed_points_rotate (n : ℕ+) :
id                                          └┘
src                                         └┘
typ                                         └┘
doc                                         └┘
113    (⟨vector.repeat (1 : G) n, one_mem_vectors_prod_eq_one n⟩ : vectors_prod_eq_one G n) ∈
id       └───────────┘          └─────────────────────────┘     └─────────────────┘    
src      └───────────┘            └─────────────────────────┘      └─────────────────┘      
typ      └───────────┘          └─────────────────────────┘     └─────────────────┘    
114    fixed_points (multiplicative (zmod n)) (vectors_prod_eq_one G n) :=
id     └──────────┘  └────────────┘  └──┘     └─────────────────┘  
src    └──────────┘  └────────────┘  └──┘      └─────────────────┘
typ    └──────────┘  └────────────┘  └──┘     └─────────────────┘  
115  λ m, subtype.eq $ vector.eq _ _ $
id       └────────┘   └───────┘
src       └────────┘   └───────┘
typ      └────────┘   └───────┘
116  by haveI : nonempty G := ⟨1⟩; exact
id              └──────┘ 
src     └──────┘└──────┘ └──┘ └┘  └────┘
typ     └──────┘└──────┘└──┘ └┘  └────┘
doc     └──────┘         └──┘ └┘  └────┘
txt     └──────┘         └──┘ └┘  └────┘
par     └──────┘         └──┘ └┘  └────┘
pid          └┘         └──┘ └┘       
st     └─────────────────────────────────
117  rotate_eq_self_iff_eq_repeat.2 ⟨(1 : G),
id   └──────────────────────────┘
src  └──────────────────────────┘└─┘  └──┘ └──
typ  └──────────────────────────┘└─┘  └──┘ └──
doc                              └─┘  └──┘ └──
txt                              └─┘  └──┘ └──
par                              └─┘  └──┘ └──
pid                              └─┘  └──┘ └──
st   ─────────────────────────────────────────
118    show list.repeat (1 : G) n = list.repeat 1 (list.repeat (1 : G) n).length, by simp⟩ _
id                                                └─────────┘        
src  ─┘                └──┘ └┘            └─┘ └─────────┘ └──┘ └┘ └───────────┘└──┘└───
typ  ─┘                └──┘ └┘            └─┘ └─────────┘ └──┘└┘└───────────┘└──┘└───
doc  ─┘                └──┘ └┘             └─┘             └──┘ └┘ └───────────┘└──┘└───
txt  ─┘                └──┘ └┘             └─┘             └──┘ └┘ └───────────┘└──┘└───
par  ─┘                └──┘ └┘             └─┘             └──┘ └┘ └───────────┘└──┘└───
pid  ─┘                └──┘ └┘             └─┘             └──┘ └┘ └──────────────────┘
st   ──────────────────────────────────────────────────────────────────────────────┘└───┘└───
119  
src  
typ  
doc  
txt  
par  
pid  
st   
120  /-- Cauchy's theorem -/
121  lemma exists_prime_order_of_dvd_card [fintype G] {p : ℕ} (hp : nat.prime p)
id                                         └─────┘                └───────┘ 
src                                        └─────┘                 └───────┘
typ                                        └─────┘                └───────┘ 
doc                                        └─────┘                  └───────┘
122    (hdvd : p ∣ card G) : ∃ x : G, order_of x = p :=
id               └──┘           └──────┘   
src               └──┘             └──────┘   
typ              └──┘           └──────┘   
doc                └──┘               └──────┘
123  let n : ℕ+ := ⟨p - 1, nat.sub_pos_of_lt hp.one_lt⟩ in
id           └┘          └───────────────┘ └┘└─────┘
src          └┘           └───────────────┘   └─────┘
typ          └┘          └───────────────┘ └┘└─────┘
doc          └┘
124  let p' : ℕ+ := ⟨p, hp.pos⟩ in
id            └┘       └┘└──┘
src           └┘          └──┘
typ           └┘       └┘└──┘
doc           └┘
125  have hn : p' = n + 1 := subtype.eq (nat.succ_sub hp.pos),
id             └┘         └────────┘  └──────────┘ └┘└──┘
src                        └────────┘  └──────────┘   └──┘
typ            └┘         └────────┘  └──────────┘ └┘└──┘
126  have hcard : card (vectors_prod_eq_one G (n + 1)) = card G ^ (n : ℕ),
id                └──┘  └─────────────────┘          └──┘       
src               └──┘  └─────────────────┘            └──┘         
typ               └──┘  └─────────────────┘          └──┘       
doc               └──┘                                   └──┘
127    by rw [set.ext mem_vectors_prod_eq_one_iff,
id            └─────┘ └─────────────────────────┘
src       └──┘└─────┘└─────────────────────────┘└─
typ       └──┘└─────┘└─────────────────────────┘└─
doc       └──┘                                  └─
txt       └──┘                                  └─
par       └──┘                                  └─
pid         └┘                                  └─
st       └──────────────────────────────────────┘└─
128      set.card_range_of_injective (mk_vector_prod_eq_one_inj _), card_vector],
id       └─────────────────────────┘  └───────────────────────┘     └─────────┘
src  ───┘└─────────────────────────┘ └───────────────────────┘└───┘└─────────┘
typ  ───┘└─────────────────────────┘ └───────────────────────┘└───┘└─────────┘
doc  ───┘                                                     └───┘           
txt  ───┘                                                     └───┘           
par  ───┘                                                     └───┘           
pid  ───┘                                                     └───┘           
st   ────────────────────────────────────────────────────────────┘└───────────┘
129  have hzmod : fintype.card (multiplicative (zmod p')) =
id                └──────────┘  └────────────┘  └──┘ └┘   
src               └──────────┘  └────────────┘  └──┘      
typ               └──────────┘  └────────────┘  └──┘ └┘   
doc               └──────────┘
130    (p' : ℕ) ^ 1 := (nat.pow_one p').symm ▸ card_fin _,
id      └┘            └─────────┘ └┘ └──┘   └──────┘
src                   └─────────┘    └──┘   └──────┘
typ     └┘            └─────────┘ └┘ └──┘   └──────┘
131  have hmodeq : _ = _ := @mul_action.card_modeq_card_fixed_points
id                          └─────────────────────────────────────┘
src                         └─────────────────────────────────────┘
typ                         └─────────────────────────────────────┘
132    (multiplicative (zmod p')) (vectors_prod_eq_one G p') _ _ _ _ _ _ 1 hp hzmod,
id      └────────────┘  └──┘ └┘    └─────────────────┘  └┘                └┘ └───┘
src     └────────────┘  └──┘       └─────────────────┘
typ     └────────────┘  └──┘ └┘    └─────────────────┘  └┘                └┘ └───┘
133  have hdvdcard : p ∣ fintype.card (vectors_prod_eq_one G (n + 1)) :=
id                     └──────────┘  └─────────────────┘    
src                     └──────────┘  └─────────────────┘      
typ                    └──────────┘  └─────────────────┘    
doc                      └──────────┘
134    calc p ∣ card G ^ 1 : by rwa nat.pow_one
id             └──┘              └─────────┘
src             └──┘           └──┘└─────────┘
typ            └──┘          └──┘└─────────┘
doc             └──┘            └──┘           
txt                             └──┘           
par                             └──┘           
pid                                           
st                             └────────────────
135    ... ∣ card G ^ (n : ℕ) : nat.pow_dvd_pow _ n.2
id           └──┘           └─────────────┘   
src  ─┘      └──┘             └─────────────┘    
typ  ─┘      └──┘           └─────────────┘   
doc  ─┘      └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
136    ... = card (vectors_prod_eq_one G (n + 1)) : hcard.symm,
id           └──┘  └─────────────────┘           └───┘└───┘
src          └──┘  └─────────────────┘                  └───┘
typ          └──┘  └─────────────────┘           └───┘└───┘
doc          └──┘
137  have hdvdcard₂ : p ∣ card (fixed_points (multiplicative (zmod p')) (vectors_prod_eq_one G p')) :=
id                      └──┘  └──────────┘  └────────────┘  └──┘ └┘    └─────────────────┘  └┘
src                      └──┘  └──────────┘  └────────────┘  └──┘       └─────────────────┘
typ                     └──┘  └──────────┘  └────────────┘  └──┘ └┘    └─────────────────┘  └┘
doc                       └──┘
138    nat.dvd_of_mod_eq_zero (hmodeq ▸ hn.symm ▸ nat.mod_eq_zero_of_dvd hdvdcard),
id     └────────────────────┘  └────┘  └┘└───┘  └────────────────────┘ └──────┘
src    └────────────────────┘            └───┘  └────────────────────┘
typ    └────────────────────┘  └────┘  └┘└───┘  └────────────────────┘ └──────┘
139  have hcard_pos : 0 < card (fixed_points (multiplicative (zmod p')) (vectors_prod_eq_one G p')) :=
id                       └──┘  └──────────┘  └────────────┘  └──┘ └┘    └─────────────────┘  └┘
src                      └──┘  └──────────┘  └────────────┘  └──┘       └─────────────────┘
typ                      └──┘  └──────────┘  └────────────┘  └──┘ └┘    └─────────────────┘  └┘
doc                       └──┘
140    fintype.card_pos_iff.2 ⟨⟨⟨vector.repeat 1 p', one_mem_vectors_prod_eq_one _⟩,
id     └──────────────────┘     └───────────┘   └┘  └─────────────────────────┘
src    └──────────────────┘     └───────────┘       └─────────────────────────┘
typ    └──────────────────┘     └───────────┘   └┘  └─────────────────────────┘
141      one_mem_fixed_points_rotate _⟩⟩,
id       └─────────────────────────┘
src      └─────────────────────────┘
typ      └─────────────────────────┘
142  have hlt : 1 < card (fixed_points (multiplicative (zmod p')) (vectors_prod_eq_one G p')) :=
id                 └──┘  └──────────┘  └────────────┘  └──┘ └┘    └─────────────────┘  └┘
src                └──┘  └──────────┘  └────────────┘  └──┘       └─────────────────┘
typ                └──┘  └──────────┘  └────────────┘  └──┘ └┘    └─────────────────┘  └┘
doc                 └──┘
143    calc (1 : ℕ) < p' : hp.one_lt
id                   └┘   └┘└─────┘
src                         └─────┘
typ                  └┘   └┘└─────┘
144    ... ≤ _ : nat.le_of_dvd hcard_pos hdvdcard₂,
id               └───────────┘ └───────┘ └───────┘
src              └───────────┘
typ              └───────────┘ └───────┘ └───────┘
145  let ⟨⟨⟨⟨x, hx₁⟩, hx₂⟩, hx₃⟩, hx₄⟩ := fintype.exists_ne_of_one_lt_card hlt
id   └─┘       └─┘   └─┘                 └──────────────────────────────┘ └─┘
src                                       └──────────────────────────────┘
typ  └─┘       └─┘   └─┘                 └──────────────────────────────┘ └─┘
146    ⟨_, one_mem_fixed_points_rotate p'⟩ in
id         └─────────────────────────┘ └┘
src        └─────────────────────────┘
typ        └─────────────────────────┘ └┘
147  have hx : x ≠ list.repeat (1 : G) p', from λ h, by simpa [h, vector.repeat] using hx₄,
id                └─────────┘        └┘                       └───────────┘        └─┘
src               └─────────┘                          └─────┘ └┘└───────────┘└──────┘
typ               └─────────┘        └┘              └─────┘└┘└───────────┘└──────┘└─┘
doc                                                     └─────┘ └┘             └──────┘
txt                                                     └─────┘ └┘             └──────┘
par                                                     └─────┘ └┘             └──────┘
pid                                                           └┘             └────┘
st                                                     └─────────────────────────────────┘
148  have nG : nonempty G, from ⟨1⟩,
id             └──────┘ 
src            └──────┘
typ            └──────┘ 
149  have ∃ a, x = list.repeat a x.length := by exactI rotate_eq_self_iff_eq_repeat.1 (λ n,
id             └─────────┘   └─────┘              └──────────────────────────┘
src             └─────────┘    └─────┘       └─────┘└──────────────────────────┘└─┘  └───
typ            └─────────┘   └─────┘       └─────┘└──────────────────────────┘└─┘  └───
doc                                             └─────┘                            └─┘  └───
txt                                             └─────┘                            └─┘  └───
par                                             └─────┘                            └─┘  └───
pid                                                                               └─┘  └───
st                                             └────────────────────────────────────────────
150    have list.rotate x (n : zmod p').val = x :=
id                                           
src  ─┘    └───────────┘   └─┘      └────┘ └───
typ  ─┘    └───────────┘   └─┘      └────┘└───
doc  ─┘    └───────────┘   └─┘      └────┘  └───
txt  ─┘    └───────────┘   └─┘      └────┘  └───
par  ─┘    └───────────┘   └─┘      └────┘  └───
pid  ─┘    └───────────┘   └─┘      └────┘  └───
st   ──────────────────────────────────────────────
151      subtype.mk.inj (subtype.mk.inj (hx₃ (n : zmod p'))),
id                       └────────────┘  └─┘      └──┘ └┘
src  ───┘               └────────────┘      └─┘└──┘  └────
typ  ───┘               └────────────┘ └─┘  └─┘└──┘└┘└────
doc  ───┘                                   └─┘      └────
txt  ───┘                                   └─┘      └────
par  ───┘                                   └─┘      └────
pid  ───┘                                   └─┘      └────
st   ─────────────────────────────────────────────────────────
152    by rwa [zmod.val_cast_nat, ← hx₁, rotate_mod] at this),
id             └───────────────┘    └─┘  └────────┘
src  ─┘  └───┘└───────────────┘└──┘   └┘└────────┘└───────┘
typ  ─┘  └───┘└───────────────┘└──┘└─┘└┘└────────┘└───────┘
doc  ─┘  └───┘                 └──┘   └┘          └───────┘
txt  ─┘  └───┘                 └──┘   └┘          └───────┘
par  ─┘  └───┘                 └──┘   └┘          └───────┘
pid  ─┘  └────┘                 └──┘   └┘          └────────┘
st   ───┘└─────────────────────┘└─────┘└──────────┘└──────┘
153  let ⟨a, ha⟩ := this in
id   └─┘    └┘     └──┘
typ  └─┘    └┘     └──┘
154  ⟨a, have hx1 : x.prod = 1 := hx₂,
id                   └───┘ 
src                  └───┘ 
typ                  └───┘ 
doc                  └───┘
155    have ha1: a ≠ 1, from λ h, hx (ha.symm ▸ h ▸ hx₁ ▸ rfl),
id                              └┘    └───┘         └─┘
src                                    └───┘          └─┘
typ                             └┘    └───┘         └─┘
156    have a ^ p = 1, by rwa [ha, list.prod_repeat, hx₁] at hx1,
id                          └┘  └──────────────┘  └─┘
src                     └───┘  └┘└──────────────┘└┘   └──────┘
typ                    └───┘└┘└┘└──────────────┘└┘└─┘└──────┘
doc                       └───┘  └┘                └┘   └──────┘
txt                       └───┘  └┘                └┘   └──────┘
par                       └───┘  └┘                └┘   └──────┘
pid                          └┘  └┘                └┘   └─────┘
st                       └──────┘└────────────────┘└───┘└─────┘
157    (hp.2 _ (order_of_dvd_of_pow_eq_one this)).resolve_left
id      └┘     └────────────────────────┘ └──┘  └──────────┘
src            └────────────────────────┘       └──────────┘
typ     └┘     └────────────────────────┘ └──┘  └──────────┘
158      (λ h, ha1 (order_of_eq_one_iff.1 h))⟩
id            └─┘  └─────────────────┘  
src                 └─────────────────┘
typ           └─┘  └─────────────────┘  
159  
160  open is_subgroup is_submonoid is_group_hom mul_action
161  
162  lemma mem_fixed_points_mul_left_cosets_iff_mem_normalizer {H : set G} [is_subgroup H] [fintype H]
id                                                                  └─┘    └─────────┘    └─────┘ 
src                                                                 └─┘     └─────────┘     └─────┘
typ                                                                 └─┘    └─────────┘    └─────┘ 
doc                                                                         └─────────┘     └─────┘
163    {x : G} : (x : quotient H) ∈ fixed_points H (quotient H) ↔ x ∈ normalizer H :=
id                  └──────┘    └──────────┘   └──────┘      └────────┘ 
src                   └──────┘     └──────────┘    └──────┘        └────────┘
typ                 └──────┘    └──────────┘   └──────┘      └────────┘ 
doc                   └──────┘                      └──────┘
164  ⟨λ hx, have ha : ∀ {y : quotient H}, y ∈ orbit H (x : quotient H) → y = x,
id      └┘                   └──────┘      └───┘      └──────┘       
src                          └──────┘        └───┘        └──────┘        
typ     └┘                   └──────┘      └───┘      └──────┘       
doc                          └──────┘                      └──────┘
165    from λ _, ((mem_fixed_points' _).1 hx _),
id                └───────────────┘     └┘
src                └───────────────┘   
typ               └───────────────┘     └┘
166    (inv_mem_iff _).1 (mem_normalizer_fintype (λ n hn,
id      └─────────┘      └────────────────────┘     └┘
src     └─────────┘      └────────────────────┘
typ     └─────────┘      └────────────────────┘     └┘
167      have (n⁻¹ * x)⁻¹ * x ∈ H := quotient_group.eq.1 (ha (mem_orbit _ ⟨n⁻¹, inv_mem hn⟩)),
id             └┘   └┘        └───────────────┘   └┘  └───────┘    └┘  └─────┘ └┘
src             └┘    └┘          └───────────────┘       └───────┘     └┘  └─────┘
typ            └┘   └┘        └───────────────┘   └┘  └───────┘    └┘  └─────┘ └┘
168      by simpa only [mul_inv_rev, inv_inv] using this)),
id                      └─────────┘  └─────┘        └──┘
src         └──────────┘└─────────┘└┘└─────┘└──────┘
typ         └──────────┘└─────────┘└┘└─────┘└──────┘└──┘
doc         └──────────┘           └┘       └──────┘
txt         └──────────┘           └┘       └──────┘
par         └──────────┘           └┘       └──────┘
pid              └──┘└┘           └┘       └────┘
st         └───────────────────────────────────────────┘
169  λ (hx : ∀ (n : G), n ∈ H ↔ x * n * x⁻¹ ∈ H),
id                            └┘  
src                                  └┘ 
typ                           └┘  
170  (mem_fixed_points' _).2 $ λ y, quotient.induction_on' y $ λ y hy, quotient_group.eq.2
id    └───────────────┘           └────────────────────┘       └┘  └───────────────┘
src   └───────────────┘            └────────────────────┘             └───────────────┘
typ   └───────────────┘           └────────────────────┘       └┘  └───────────────┘
171    (let ⟨⟨b, hb₁⟩, hb₂⟩ := hy in
id      └─┘     └─┘   └─┘     └┘
typ     └─┘     └─┘   └─┘     └┘
172    have hb₂ : (b * x)⁻¹ * y ∈ H := quotient_group.eq.1 hb₂,
id                     └┘        └───────────────┘
src                     └┘          └───────────────┘
typ                    └┘        └───────────────┘
173    (inv_mem_iff H).1 $ (hx _).2 $ (mul_mem_cancel_right H (inv_mem hb₁)).1
id      └─────────┘       └┘        └──────────────────┘   └─────┘      
src     └─────────┘                  └──────────────────┘    └─────┘      
typ     └─────────┘       └┘        └──────────────────┘   └─────┘      
174    $ by rw hx at hb₂;
id             └┘
src         └─┘  └─────┘
typ         └─┘└┘└─────┘
doc         └─┘  └─────┘
txt         └─┘  └─────┘
par         └─┘  └─────┘
pid             └─────┘
st         └──────────────
175      simpa [mul_inv_rev, mul_assoc] using hb₂)⟩
id              └─────────┘  └───────┘        └─┘
src      └─────┘└─────────┘└┘└───────┘└──────┘
typ      └─────┘└─────────┘└┘└───────┘└──────┘└─┘
doc      └─────┘           └┘         └──────┘
txt      └─────┘           └┘         └──────┘
par      └─────┘           └┘         └──────┘
pid                      └┘         └────┘
st   ───────────────────────────────────────────┘
176  
177  def fixed_points_mul_left_cosets_equiv_quotient (H : set G) [is_subgroup H] [fintype H] :
id                                                        └─┘    └─────────┘    └─────┘ 
src                                                       └─┘     └─────────┘     └─────┘
typ                                                       └─┘    └─────────┘    └─────┘ 
doc                                                               └─────────┘     └─────┘
178    fixed_points H (quotient H) ≃ quotient (subtype.val ⁻¹' H : set (normalizer H)) :=
id     └──────────┘   └──────┘    └──────┘  └─────────┘ └─┘    └─┘  └────────┘ 
src    └──────────┘    └──────┘     └──────┘  └─────────┘ └─┘     └─┘  └────────┘
typ    └──────────┘   └──────┘    └──────┘  └─────────┘ └─┘    └─┘  └────────┘ 
doc                    └──────┘     └──────┘              └─┘
179  @subtype_quotient_equiv_quotient_subtype G (normalizer H) (id _) (id _) (fixed_points _ _)
id    └─────────────────────────────────────┘   └────────┘    └┘     └┘     └──────────┘
src   └─────────────────────────────────────┘    └────────┘     └┘     └┘     └──────────┘
typ   └─────────────────────────────────────┘   └────────┘    └┘     └┘     └──────────┘
180    (λ a, mem_fixed_points_mul_left_cosets_iff_mem_normalizer.symm) (by intros; refl)
id          └─────────────────────────────────────────────────┘└───┘
src          └─────────────────────────────────────────────────┘└───┘      └────┘  └──┘
typ         └─────────────────────────────────────────────────┘└───┘      └────┘  └──┘
doc                                                                        └────┘  └──┘
txt                                                                        └────┘  └──┘
par                                                                        └────┘  └──┘
st                                                                        └───────────┘
181  
182  local attribute [instance] set_fintype
id                              └─────────┘
src                             └─────────┘
typ                             └─────────┘
183  
184  lemma exists_subgroup_card_pow_prime [fintype G] {p : ℕ} : ∀ {n : ℕ} (hp : nat.prime p)
id                                         └─────┘                          └───────┘ 
src                                        └─────┘                            └───────┘
typ                                        └─────┘                          └───────┘ 
doc                                        └─────┘                              └───────┘
185    (hdvd : p ^ n ∣ card G), ∃ H : set G, is_subgroup H ∧ fintype.card H = p ^ n
id                 └──┘         └─┘  └─────────┘   └──────────┘     
src                  └──┘          └─┘   └─────────┘    └──────────┘      
typ                └──┘         └─┘  └─────────┘   └──────────┘     
doc                    └──┘                  └─────────┘     └──────────┘
186  | 0 := λ _ _, ⟨trivial G, by apply_instance, by simp⟩
id                └─────┘ 
src                 └─────┘       └────────────┘     └──┘
typ               └─────┘      └────────────┘     └──┘
doc                 └─────┘       └────────────┘     └──┘
txt                               └────────────┘     └──┘
par                               └────────────┘     └──┘
st                               └─────────────┘    └───┘
187  | (n+1) := λ hp hdvd,
id               └┘ └──┘
src      
typ              └┘ └──┘
188  let ⟨H, ⟨hH1, hH2⟩⟩ := exists_subgroup_card_pow_prime hp
id   └─┘                    └────────────────────────────┘ └┘
typ  └─┘                    └────────────────────────────┘ └┘
189    (dvd.trans (nat.pow_dvd_pow _ (nat.le_succ _)) hdvd) in
id      └───────┘  └─────────────┘    └─────────┘     └──┘
src     └───────┘  └─────────────┘    └─────────┘
typ     └───────┘  └─────────────┘    └─────────┘     └──┘
190  let ⟨s, hs⟩ := exists_eq_mul_left_of_dvd hdvd in
id   └─┘            └───────────────────────┘ └──┘
src                 └───────────────────────┘
typ  └─┘            └───────────────────────┘ └──┘
191  by exactI
src     └─────┘
typ     └─────┘
doc     └─────┘
txt     └─────┘
par     └─────┘
pid           
st     └───────
192  have hcard : card (quotient H) = s * p :=
id                                     
src      └───────┘              └┘  └───
typ      └───────┘              └┘  └───
doc      └───────┘              └┘    └───
txt      └───────┘              └┘    └───
par      └───────┘              └┘    └───
pid      └───────┘              └┘    └───
st   ──────────────────────────────────────────
193    (nat.mul_right_inj (show card H > 0, from fintype.card_pos_iff.2
id      └───────────────┘       └──┘            └──────────────────┘
src  ─┘ └───────────────┘     └──┘ └───────┘└──────────────────┘└──
typ  ─┘ └───────────────┘     └──┘ └───────┘└──────────────────┘└──
doc  ─┘                       └──┘  └───────┘                    └──
txt  ─┘                             └───────┘                    └──
par  ─┘                             └───────┘                    └──
pid  ─┘                             └───────┘                    └──
st   ───────────────────────────────────────────────────────────────────
194        ⟨⟨1, is_submonoid.one_mem H⟩⟩)).1
id              └──────────────────┘ 
src  ─────┘  └─┘└──────────────────┘ └──────
typ  ─────┘  └─┘└──────────────────┘└──────
doc  ─────┘  └─┘                     └──────
txt  ─────┘  └─┘                     └──────
par  ─────┘  └─┘                     └──────
pid  ─────┘  └─┘                     └──────
st   ────────────────────────────────────────
195      (by rwa [← card_eq_card_quotient_mul_card_subgroup, hH2, hs,
id                  └─────────────────────────────────────┘  └─┘  └┘
src  ───┘   └─────┘└─────────────────────────────────────┘└┘   └┘  └─
typ  ───┘   └─────┘└─────────────────────────────────────┘└┘└─┘└┘└┘└─
doc  ───┘   └─────┘                                       └┘   └┘  └─
txt  ───┘   └─────┘                                       └┘   └┘  └─
par  ───┘   └─────┘                                       └┘   └┘  └─
pid  ───┘   └──────┘                                       └┘   └┘  └─
st   ──────┘└─────────────────────────────────────────────┘└───┘└──┘└─
196        nat.pow_succ, mul_assoc, mul_comm p]),
id         └──────────┘  └───────┘  └──────┘ 
src  ─────┘└──────────┘└┘└───────┘└┘└──────┘ └─┘
typ  ─────┘└──────────┘└┘└───────┘└┘└──────┘└─┘
doc  ─────┘            └┘         └┘         └─┘
txt  ─────┘            └┘         └┘         └─┘
par  ─────┘            └┘         └┘         └─┘
pid  ─────┘            └┘         └┘         └──┘
st   ─────────────────┘└─────────┘└──────────┘└──
197  have hm : s * p % p = card (quotient (subtype.val ⁻¹' H : set (normalizer H))) % p :=
id                                                   └─┘
src      └────┘                              └─┘ └─┘               └──┘  └───
typ      └────┘                             └─┘ └─┘               └──┘  └───
doc      └────┘                               └─┘ └─┘               └──┘  └───
txt      └────┘                                   └─┘               └──┘  └───
par      └────┘                                   └─┘               └──┘  └───
pid      └────┘                                   └─┘               └──┘  └───
st   ──────────────────────────────────────────────────────────────────────────────────────
198    card_congr (fixed_points_mul_left_cosets_equiv_quotient H) ▸ hcard ▸
id     └────────┘  └─────────────────────────────────────────┘    
src  ─┘└────────┘ └─────────────────────────────────────────┘ └┘      
typ  ─┘└────────┘ └─────────────────────────────────────────┘ └┘      
doc  ─┘                                                       └┘       
txt  ─┘                                                       └┘       
par  ─┘                                                       └┘       
pid  ─┘                                                       └┘       
st   ───────────────────────────────────────────────────────────────────────
199      card_modeq_card_fixed_points hp hH2,
id       └──────────────────────────┘ └┘ └─┘
src  ───┘└──────────────────────────┘     └┘
typ  ───┘└──────────────────────────┘└┘└─┘└┘
doc  ───┘                                 └┘
txt  ───┘                                 └┘
par  ───┘                                 └┘
pid  ───┘                                 └┘
st   ─────────────────────────────────────────
200  have hm' : p ∣ card (quotient (subtype.val ⁻¹' H : set (normalizer H))) :=
id                       └──────┘
src      └─────┘      └──────┘                └─┘               └──────
typ      └─────┘      └──────┘                └─┘               └──────
doc      └─────┘       └──────┘                └─┘               └──────
txt      └─────┘                               └─┘               └──────
par      └─────┘                               └─┘               └──────
pid      └─────┘                               └─┘               └──────
st   ───────────────────────────────────────────────────────────────────────────
201    nat.dvd_of_mod_eq_zero
id     └────────────────────┘
src  ─┘└────────────────────┘
typ  ─┘└────────────────────┘
doc  ─┘                      
txt  ─┘                      
par  ─┘                      
pid  ─┘                      
st   ─────────────────────────
202      (by rwa [nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm),
id                └────────────────────┘  └──────────┘       └─────┘
src  ───┘   └───┘└────────────────────┘ └──────────┘└─────┘└─────┘└─────┘└─┘
typ  ───┘   └───┘└────────────────────┘ └──────────┘└─────┘└─────┘└─────┘└─┘
doc  ───┘   └───┘                                   └─────┘       └─────┘└─┘
txt  ───┘   └───┘                                   └─────┘       └─────┘└─┘
par  ───┘   └───┘                                   └─────┘       └─────┘└─┘
pid  ───┘   └────┘                                   └─────┘       └────────┘
st   ──────┘└─────────────────────────────────────────────┘└───────┘└────┘└──
203  let ⟨x, hx⟩ := @exists_prime_order_of_dvd_card _ (quotient_group.group _) _ _ hp hm' in
id                  └────────────────────────────┘    └──────────────────┘
src       └┘  └───┘ └────────────────────────────┘└─┘ └──────────────────┘└──────┘     └──┘
typ      └┘  └───┘ └────────────────────────────┘└─┘ └──────────────────┘└──────┘     └──┘
doc       └┘  └───┘ └────────────────────────────┘└─┘                     └──────┘     └──┘
txt       └┘  └───┘                               └─┘                     └──────┘     └──┘
par       └┘  └───┘                               └─┘                     └──────┘     └──┘
pid       └┘  └───┘                               └─┘                     └──────┘     └──┘
st   ────────────────────────────────────────────────────────────────────────────────────────
204  have hxcard : ∀ {f : fintype (gpowers x)}, card (gpowers x) = p,
id                        └─────┘                                  
src      └────────┘ └────┘                └┘              └┘  └─
typ      └────────┘ └────┘└─────┘         └┘              └┘ └─
doc      └────────┘ └────┘                └┘              └┘  └─
txt      └────────┘ └────┘                └┘              └┘  └─
par      └────────┘ └────┘                └┘              └┘  └─
pid      └────────┘ └────┘                └┘              └┘  └─
st   ─────────────────────────────────────────────────────────────────
205    from λ f, by rw [← hx, order_eq_card_gpowers]; congr,
id                        └┘  └───────────────────┘
src  ──────┘ └──┘  └────┘  └┘└───────────────────┘└┘└───┘└┘
typ  ──────┘ └──┘  └────┘└┘└┘└───────────────────┘└┘└───┘└┘
doc  ──────┘ └──┘  └────┘  └┘                     └┘     └┘
txt  ──────┘ └──┘  └────┘  └┘                     └┘└───┘└┘
par  ──────┘ └──┘  └────┘  └┘                     └┘└───┘└┘
pid  ──────┘ └──┘  └─────┘  └┘                     └────────┘
st   ─────────────┘└───────┘└─────────────────────┘└─────┘└─
206  have is_subgroup (mk ⁻¹' gpowers x),
src      └───────────┘              └──
typ      └───────────┘              └──
doc      └───────────┘              └──
txt      └───────────┘              └──
par      └───────────┘              └──
pid      └───────────┘              └──
st   ─────────────────────────────────────
207    from is_group_hom.preimage _ _,
id          └───────────────────┘
src  ──────┘└───────────────────┘└────┘
typ  ──────┘└───────────────────┘└────┘
doc  ──────┘                     └────┘
txt  ──────┘                     └────┘
par  ──────┘                     └────┘
pid  ──────┘                     └────┘
st   ──────────────────────────────────
208  have fintype (mk ⁻¹' gpowers x), by apply_instance,
src      └───────┘              └────┘└────────────┘└┘
typ      └───────┘              └────┘└────────────┘└┘
doc      └───────┘              └────┘└────────────┘└┘
txt      └───────┘              └────┘└────────────┘└┘
par      └───────┘              └────┘└────────────┘└┘
pid      └───────┘              └────────────────────┘
st   ──────────────────────────────────┘└─────────────┘└─
209  have hequiv : H ≃ (subtype.val ⁻¹' H : set (normalizer H)) :=
id                                         └─┘  └────────┘
src      └────────┘                 └─┘└─┘ └────────┘ └─────
typ      └────────┘                 └─┘└─┘ └────────┘ └─────
doc      └────────┘                 └─┘               └─────
txt      └────────┘                  └─┘               └─────
par      └────────┘                  └─┘               └─────
pid      └────────┘                  └─┘               └─────
st   ──────────────────────────────────────────────────────────────
210    ⟨λ a, ⟨⟨a.1, subset_normalizer _ a.2⟩, a.2⟩, λ a, ⟨a.1.1, a.2⟩,
id                  └───────────────┘
src  ─┘  └──┘   └──┘└───────────────┘└─┘ └───┘ └───┘ └──┘  └────┘ └────
typ  ─┘  └──┘   └──┘└───────────────┘└─┘ └───┘ └───┘ └──┘  └────┘ └────
doc  ─┘  └──┘   └──┘                 └─┘ └───┘ └───┘ └──┘  └────┘ └────
txt  ─┘  └──┘   └──┘                 └─┘ └───┘ └───┘ └──┘  └────┘ └────
par  ─┘  └──┘   └──┘                 └─┘ └───┘ └───┘ └──┘  └────┘ └────
pid  ─┘  └──┘   └──┘                 └─┘ └───┘ └───┘ └──┘  └────┘ └────
st   ──────────────────────────────────────────────────────────────────
211      λ ⟨_, _⟩, rfl, λ ⟨⟨_, _⟩, _⟩, rfl⟩,
id                                     └─┘
src  ───┘ └───────┘   └┘ └┘ └─────────┘└─┘└─┘
typ  ───┘ └───────┘   └┘ └┘ └─────────┘└─┘└─┘
doc  ───┘ └───────┘   └┘ └┘ └─────────┘   └─┘
txt  ───┘ └───────┘   └┘ └┘ └─────────┘   └─┘
par  ───┘ └───────┘   └┘ └┘ └─────────┘   └─┘
pid  ───┘ └───────┘   └┘ └┘ └─────────┘   └─┘
st   ────────────────────────────────────────
212  ⟨subtype.val '' (mk ⁻¹' gpowers x), by apply_instance,
id    └─────────┘ └┘  └┘     └─────┘
src   └─────────┘└┘ └┘   └─────┘ └─┘  └────────────┘└─
typ   └─────────┘└┘ └┘   └─────┘ └─┘  └────────────┘└─
doc                              └─┘  └────────────┘└─
txt                              └─┘  └────────────┘└─
par                              └─┘  └────────────┘└─
pid                              └─┘  └────────────────
st   ─────────────────────────────────────┘└─────────────┘└─
213    by rw [set.card_image_of_injective (mk ⁻¹' gpowers x) subtype.val_injective,
id            └─────────────────────────┘  └┘     └─────┘   └───────────────────┘
src  ─┘  └──┘└─────────────────────────┘ └┘   └─────┘ └┘└───────────────────┘└─
typ  ─┘  └──┘└─────────────────────────┘ └┘   └─────┘└┘└───────────────────┘└─
doc  ─┘  └──┘                                         └┘                     └─
txt  ─┘  └──┘                                         └┘                     └─
par  ─┘  └──┘                                         └┘                     └─
pid  ─┘  └───┘                                         └┘                     └─
st   ───┘└───────────────────────────────────────────────────────────────────────┘└─
214        nat.pow_succ, ← hH2, fintype.card_congr hequiv, ← hx, order_eq_card_gpowers,
id         └──────────┘    └─┘  └────────────────┘ └────┘    └┘  └───────────────────┘
src  ─────┘└──────────┘└──┘   └┘└────────────────┘      └──┘  └┘└───────────────────┘└─
typ  ─────┘└──────────┘└──┘└─┘└┘└────────────────┘└────┘└──┘└┘└┘└───────────────────┘└─
doc  ─────┘            └──┘   └┘                        └──┘  └┘                     └─
txt  ─────┘            └──┘   └┘                        └──┘  └┘                     └─
par  ─────┘            └──┘   └┘                        └──┘  └┘                     └─
pid  ─────┘            └──┘   └┘                        └──┘  └┘                     └─
st   ─────────────────┘└─────┘└─────────────────────────┘└────┘└─────────────────────┘└─
215        ← fintype.card_prod];
id           └───────────────┘
src  ───────┘└───────────────┘└─
typ  ───────┘└───────────────┘└─
doc  ───────┘                 └─
txt  ───────┘                 └─
par  ───────┘                 └─
pid  ───────┘                 └──
st   ────────────────────────┘└─
216      exact @fintype.card_congr _ _ (id _) (id _) (preimage_mk_equiv_subgroup_times_set _ _)⟩
id              └────────────────┘             └┘     └──────────────────────────────────┘
src  ───┘└────┘ └────────────────┘└───┘   └──┘ └┘└──┘ └──────────────────────────────────┘└───┘└─
typ  ─────────┘ └────────────────┘└───┘   └──┘ └┘└──┘ └──────────────────────────────────┘└──────
doc  ───┘└────┘                   └───┘   └──┘   └──┘                                     └───┘└─
txt  ───┘└────┘                   └───┘   └──┘   └──┘                                     └───┘└─
par  ─────────┘                   └───┘   └──┘   └──┘                                     └──────
pid  ─────────┘                   └───┘   └──┘   └──┘                                     └────┘
st   ─────────────────────────────────────────────────────────────────────────────────────────┘└─
217  
src  
typ  
doc  
txt  
par  
pid  
st   
218  end sylow